(declare-fun a () Int)
(declare-fun b () String)
(declare-fun c () Int)
(declare-fun d () Bool)
(declare-fun e () Int)
(declare-fun f () Bool)
(assert (= (not (= (div a e) (- 1))) (= c 0)))
(assert (= c (- 1) d))
(assert d)
(assert (= f (not (= e (- 1)))))
(assert (ite f (= (str.substr b 0 0) "ptrackp=") (= (div a c) (- 1))))
(check-sat)
